%%%%%%%%%%%%%%%%%%%%% chapter.tex %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% sample chapter
%
% Use this file as a template for your own input.
%
%%%%%%%%%%%%%%%%%%%%%%%% Springer-Verlag %%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Introduction}
\label{intro} % Always give a unique label
% use \chaptermark{}
% to alter or adjust the chapter heading in the running head

Buffer overflow attacks have existed at least since 1988, when a
buffer overflow vulnerability in finger was exploited. Although
researchers quickly discovered how the attack worked and how to
protect systems against them, buffer overflow vulnerabilities
continued to exist. It became apparent that programming in C
without introducing these vulnerabilities is almost impossible for
humans, so subsequent languages have included dynamic array
bounds checking. Such checks are effective but greatly diminish the
speed of a program's execution. The result is that programmers
at present must choose between security and speed.

In many cases, speed is not essential and programmers are content
to let their programs take whatever time is necessary to execute.
However, this is not always possible: programmers in systems, video
games, and other fields must coax every bit of performance out of
their programs. Because they need the performance, they are forced
to use C (or a variant) and then to try to program securely.

The continual need for security updates to every major operating
system, no matter the quality controls that go into it, is sufficient
evidence that current techniques do not suffice to secure C code.

In order to produce programs that are both performant and secure,
some technique must eliminate the performance bottleneck in
programs written in secure (with respect to buffer overflows)
languages or some technique must secure C programs.

Many languages have advanced techniques that grant them
significant speedups; for example, Java does JIT compilation. But
none of these techniques grants enough speed to programs (at
least, to programs in general) to make these languages useful
in performance-dependent fields.

Assuming for the time being that such a speedup cannot be done,
we are left with the task of securing C code. It is relatively simple
to secure C code by automatically adding checks to every array
reference, but such an approach slows the programs down.

A static analysis of a C program could prove that it is secure
against buffer overflows without affecting the execution time of
the program. Programmers could write as usual, check their
programs for vulnerabilities with a static analyzer, modify their
code to ensure security, and repeat the process until the program
is proven secure. This is a time-consuming process, but it is
certain to be preferable to releasing and subsequently patching
a program.

Being static, this analysis cannot be perfectly precise; the halting
problem makes it impossible. Instead, it must be a conservative
approximation that reports possible vulnerabilities.

In this paper, we discuss a static analyzer that serves as a proof
of concept. It analyzes programs written in a small subset of C.
We claim that this subset is representative of the language as a
whole. We describe the functionality of the static analyzer, show
the results it gives, and discuss its soundness and the certainty
that it terminates.

%\section{Section Heading}
%\label{sec:1}
% Always give a unique label
% and use \ref{<label>} for cross-references
% and \cite{<label>} for bibliographic references
% use \sectionmark{}
% to alter or adjust the section heading in the running head
%Your text goes here. Use the \LaTeX\ automatism for your citations
%\cite{monograph}.

%\subsection{Subsection Heading}
%\label{sec:2}
%Your text goes here.

%\begin{equation}
%\vec{a}\times\vec{b}=\vec{c}
%\end{equation}

%\subsubsection{Subsubsection Heading}
%Your text goes here. Use the \LaTeX\ automatism for cross-references as
%well as for your citations, see Sect.~\ref{sec:1}.

%\paragraph{Paragraph Heading} %
%Your text goes here.

%\subparagraph{Subparagraph Heading.} Your text goes here.%
%
%\index{paragraph}
% Use the \index{} command to code your index words
%
% For tables use
%
%\begin{table}
%\centering
%\caption{Please write your table caption here}
%\label{tab:1}       % Give a unique label
%
% For LaTeX tables use
%
%\begin{tabular}{lll}
%\hline\noalign{\smallskip}
%first & second & third  \\
%\noalign{\smallskip}\hline\noalign{\smallskip}
%number & number & number \\
%number & number & number \\
%\noalign{\smallskip}\hline
%\end{tabular}
%\end{table}
%
%
% For figures use
%
%\begin{figure}
%\centering
% Use the relevant command for your figure-insertion program
% to insert the figure file.
% For example, with the option graphics use
%\includegraphics[height=4cm]{figure.eps}
%
% If not, use
%\picplace{5cm}{2cm} % Give the correct figure height and width in cm
%
%\caption{Please write your figure caption here}
%\label{fig:1}       % Give a unique label
%\end{figure}
%
% For built-in environments use
%
%\begin{theorem}
%Theorem text goes here.
%\end{theorem}
%
% or
%
%\begin{lemma}
%Lemma text goes here.
%\end{lemma}
%
%
% Problems or Exercises should be sorted chapterwise
%\section*{Problems}
%\addcontentsline{toc}{section}{Problems}
%
% Use the following environment.
% Don't forget to label each problem;
% the label is needed for the solutions' environment
%\begin{prob}
%\label{prob1}
%The problem\footnote{Footnote} is described here. The
%problem is described here. The problem is described here.
%\end{prob}

%\begin{prob}
%\label{prob2}
%\textbf{Problem Heading}\\
%(a) The first part of the problem is described here.\\
%(b) The second part of the problem is described here.
%\end{prob}



%
